T:Type. 
subtype_rel(T; )  (bs,as:(T List), x:T. (x  merge(as; bs))  ((x  as)  (x  bs))) 

latex

Definitions	(x  l), P  Q, x:A. B(x), False, t  T, prop{i:l}, P  Q, merge(as; bs), P  Q, P  Q, P  Q, x. t(x), s-insert(x; l), guard(T)
Lemmas	nil member, member-s-insert, s-insert wf, all functionality wrt iff, iff functionality wrt iff, or functionality wrt iff, cons member, false wf, iff wf, merge wf, l member wf